package com.googlecode.kipler.container.dl.operational;

import com.googlecode.kipler.container.dl.FormulaBase;
import com.googlecode.kipler.container.dl.Individual;
import com.googlecode.kipler.container.dl.SHOIQABox;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.syntax.concept.Nominal;
import com.googlecode.kipler.syntax.formula.ConceptAssertion;
import com.googlecode.kipler.syntax.formula.Formula;


/**
 * 
 * @author İnanç Seylan
 *
 */
public class NominalMaintainingObserver implements ABoxChangeObserver {

	public void afterFormulaIsAdded(FormulaBase base, Formula formula)
			throws UnsatisfiableException {
		if (formula instanceof ConceptAssertion) {
			ConceptAssertion ca = (ConceptAssertion) formula;
			if (ca.getConcept() instanceof Nominal) {
				Nominal nominal = (Nominal) ca.getConcept();
				if (!nominal.isNegated()) {
					SHOIQABox abox = (SHOIQABox) base;
					abox.getNominals().add(abox.getIndividual(ca.getName()));
				}
			}
		}
	}

	public void afterNodeIsRemoved(FormulaBase base, Individual indv) {
		SHOIQABox abox = (SHOIQABox) base;
		if (abox.isNominal(indv)) {
			abox.getNominals().remove(indv);
		}
	}
}
